Nuprl Lemma : let_wf
12,41
postcript
pdf
A
,
B
:Type,
a
:
A
,
b
:(
A
B
). let
x
=
a
in
b
(
x
)
B
latex
ProofTree
Definitions
let
x
=
a
in
b
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
origin
A, B:Type, a:A, b:(A
B). let x = a in b(x) 
B
A, B:Type, a:A, b:(AB). let x = a in b(x) B
Tx:A. B(x)